f, g:x:Id fp Type, x:Id. x  dom(f  g)  x  dom(f)  x  dom(g) 

latex

Definitions	Id, t  T, x. t(x), x:A. B(x), a:A fp B(a), b, P  Q, P  Q, P  Q, P & Q, P  Q, x  dom(f), Prop, Top, f  g, IdDeq
Lemmas	iff functionality wrt iff, fpf-join-dom, id-deq wf, fpf-join wf, top wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, fpf wf, Id wf